CHOICE-STRATEGY-IS: 
ANCESTRY∧SUPPORT[THM];

EDIT-STRATEGY-IS: 
DEPTH[2]∨LENGTH[3];

ELAPSED-TIME =10165

NIL 1 2
1 ¬clear(C);3 12
2 clear(C);AXIOM
3 ¬(clear(B)∧clear(C));5 14
5 ¬on(B,C);7 8
7 ¬(on(x,A)∧on(B,C));9 10
8 on(C,A);AXIOM
9 ¬(on(B,C)∧clear(A));11 12
10 on(y,x)⊃clear(x);AXIOM
11 ¬(on(B,C)∧(clear(A)∧clear(B)));13 14
12 clear(B);AXIOM
13 ¬(on(B,C)∧on(A,B));THM
14 clear(x)∧clear(y)⊃on(x,y);AXIOM